Email: j.gancher@northeastern.edu
CV | Publications | Teaching | Students

Joshua Gancher

Assistant Professor
Northeastern University
Office: WVH 332

I apply tools from Formal Methods and Programming Languages to construct and certify secure systems -- particularly systems that use cryptography. Broadly, I am interested in applied cryptography, distributed systems, type systems, proof assistants, and compiler correctness.

Teaching

Students

Publications:
Concrete Security Bounds for Simulation-Based Proofs of Multi-Party Computation Protocols.
Kristina Sojakova, Mihai Codescu, and Joshua Gancher.
ILA: Correctness via Type Checking for Fully Homomorphic Encryption.
ACM CCS 2025.
Tarakaram Gollamudi, Anitha Gollamudi, and Joshua Gancher.
Vest: Verified, Secure, High-Performance Parsing and Serialization for Rust.
USENIX Security 2025.
Yi Cai, Pratap Singh, Zhengyao Lin, Jay Bosamiya, Joshua Gancher, Milijana Surbatovich, and Bryan Parno.
Towards Practical, End-to-End Formally Verified X.509 Certificate Validators with Verdict
USENIX Security 2025.
Zhengyao Lin, Michael McLoughlin, Pratap Singh, Rory Brennan-Jones, Paul Hitchcox, Joshua Gancher, and Bryan Parno.
OwlC: Compiling Security Protocols to Verified, Secure, High-Performance Libraries.
USENIX Security 2025.
Pratap Singh, Joshua Gancher, and Bryan Parno.
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions.
OOPSLA 2024.
Zhengyao Lin, Joshua Gancher, and Bryan Parno.
Secure Synthesis of Distributed Cryptographic Applications.
CSF 2024.
Coşku Acay, Josua Gancher, Rolph Recto, and Andrew Myers.
Owl: Compositional Verification of Security Protocols via an Information-Flow Type System.
IEEE S&P 2023.
Joshua Gancher, Sydney Gibson, Pratap Singh, Samvid Dharanikota, and Bryan Parno. Project link here.
A Core Calculus for Equational Proofs of Cryptographic Protocols.
POPL 2023.
Joshua Gancher, Kristina Sojakova, Xiong Fan, Elaine Shi, and Greg Morrisett. Project link here.
Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs.
PLDI 2021.
Coşku Acay, Rolph Recto, Joshua Gancher, Andrew Myers, and Elaine Shi. Project link here.
Symbolic Proofs for Lattice-Based Cryptography.
CCS 2018.
Gilles Barthe, Xiong Fan, Joshua Gancher, Benjamin Grégoire, Charlie Jacomme and Elaine Shi.
Externally Verifiable Oblivious RAM.
PETS 2017.
Joshua Gancher, Adam Groce, and Alex Ledger.